COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Typed logic
C00007 ENDMK
C⊗;
Typed logic
  u, u-i, u0, u1, u2, ...	Satisfy Unitp, i.e. represents Units
  s, s-i, s0, s1, s2, ...	Satisfy Slotp, i.e. represents Slots 
				(subtype of Units)
  f, f-i, f0, f1, f2, ...	represents Functions
  l, l-i, l0, l1, l2, ...	Satisfy LISTP, i.e. represents Lists
  t, t-i, t0, t1, t2, ...	represents Times
[ p's are used for pseudo-slots ]

	LISP OVERHEAD:
	[Note- this is essentially MEMB]
∀ v,l. v in l ≡ [ (l ≠ NIL) & ( v = CAR(l) ∨ v in CDR(l) )]

	Slot Related Overhead:

∀ s. HighLevelDefn( s ) = GetValue( s,'HighLevelDefn )
∀ s. Format( s ) = GetValue( s,'Format )
∀ s. Defn( s ) = GetValue( s,'Defn )
∀ s. Domain( s ) = GetValue( s,'Domain )
∀ s. Range( s ) = GetValue( s,'Range )
∀ u,s. GetValue-1( u,s ) = GetValue( u,s )
∀ u,s. GetValue( u,s ) = OR( UA-GETVALUE( u,s ), APPLY( Defn( s ), u ) )

∀ p. Format( p ) = CAR( Range( p ))
∀ p,HLD. HighLevelDefn( p ) = HLD ⊃
  Parse( HLD ) = LIST( Defn( p ), Range( p ), Domain( p ), ? ).

∀ u,p. GetValue-1( u,p ) = APPLY( Defn( p ),u ).

∀ u,p,v. InValue( u,p,v ) ≡
  { [ (Format( p ) ε {FSingleton} ) & v = GetValue-1( u,p ) ]
    [ (Format( p ) ε {FSet, FList} ) & v in GetValue-1( u,p ) ] }

	CONSISTENCY:
∀ u,s,v,v',t0,t1,t2. 
  [ UA-PUTVALUE( u,s,v )(t0) & [t0<t1<t2 ⊃ ¬UA-PUTVALUE( u,s,v' )(t1) ] ] ⊃
	UA-GETVALUE( u,s )(t2) = v.

∀ u,s,v,v',t0,t1,t2. 
  [ PutValue( u,s,v )(t0) & [t0<t1<t2 ⊃ ¬PutValue( u,s,v' )(t1) ] ] ⊃
	GetValue( u,s )(t2) = v.

∀ s1,s2. s2 = GetValue( s1,'Inverse ) ⊃
  [∀ u,v. InValue( u1,s,v ) ⊃ [Unitp( v ) & InValue( v,s2,u )] ]

SLOT DEFINATION:

	COMPOSITION:
∀ p1,HLD,u. HLD = HighLevelDefn( p1 ) & Composition = CAR( HLD ) ⊃
  ∃ p2. HighLevelDefn( p2 ) = CAR (CDR ( HLD ) ) &
  [IF CDR( CDR( HLD ) ) = NIL
     THEN GetValue-1( u,p1 ) = GetValue-1( u,p2 )
     ELSE ∃ p3. HighLevelDefn( p3 ) = CONS('Composition, CDR( CDR (HLD) ) )] &
	    ∀ v. InValue( u,p2,v ) ⊃
		Unitp( v ) & GetValue-1( v,p3 ) = GetValue-1( u,p1 )

	UNIONING:
∀ p1,HLD,u. HLD = HighLevelDefn( p1 ) & Composition = CAR( HLD ) ⊃
  [∃ p2. HighLevelDefn( p2 ) = CAR (CDR ( HLD ) ) &
	∀ v. InValue( u,p2,v ) ⊃ InValue( u,p1,v )] &
  [IF CDR( CDR( HLD ) ) ≠ NIL
     THEN ∃ p3. HighLevelDefn( p3 ) = CONS('Unioning, CDR( CDR (HLD) ) )] &
	    ∀ v. InValue( u,p2,v ) ⊃ InValue( u,p1,v )

	STARRING:
∀ p1,HLD,u. HLD = HighLevelDefn( p1 ) & Starring = CAR( HLD ) ⊃
  InValue( u,p2,u ) &
  ∃ p2. HighLevelDefn( p2 ) = CAR (CDR ( HLD ) ) &
     ∀ v,v1. InValue( u,p2,v ) ⊃
	Unitp( v ) & [InValue( v,p1,v1 ) ⊃ InValue( u,p1,v1 ) ]